perm filename PROVER.NOT[1,JRA] blob
sn#033001 filedate 1973-04-03 generic text, type T, neo UTF8
00100 THE RITUAL FOR CONSTRUCTION THE PROVER IS COMPLICATED BY THE
00200 USE OF A SYNTAX DIRECTED I/O (SDIO)PACKAGE FOR THE PARSERS.
00300 THE RESULTING FLEXIBILITY AS PROVED TO BE WORTH THE EXTRA HASSLE.
00400
00500 FILES:
00600 PROVE1.NEW LISP VERSION OF THE PROVER. THIS SHOULD BE COMPILED
00700 WITH FILE NAMED SPECIA.
00800 R COMPLR...(DSKIN SPECIA)...(COMPL(PROVE1.NEW))
00900
00950 MATCHE.NEW THE SEMANTIC ROUTINES FOR THE MATCHER
01000
01100 PROVER.PRM PRIMITIVE LAP ROUTINES
01200
01300 SDIO LISP PRIMITIVES FOR SDIO PACKAGE.
01400
01500 SCAN &PRIM MACHINE LANG PRIMITIVES FOR SDIO
01600
01700 UNIF MACHINE LANGUAGE PRIMITIVES FOR PROVER.
01800
01900 STATEV INITIALIZATION H.S.
02000
02100 COMMAND & EDIT & INFIX & MATCH.LSP
02200 THESE ARE THE LISP FILES FOR THE SDIO PACKAGE
02300 IF YOU WANT THE DOCUMENTATION FOR SDIO AND THE
02400 FILES WHICH GENERATE THE PARSERS THEY CAN BE SPPLIED.
02500
02600 FIX.LSP SDIO ISN'T PERFECT. THESE FILES MAKE IT SO.
02700 SDIOMA MACROS NECESSARY FOR COMPILATION OF ANY OF THE SDIO
02800 FILES.
02900
03000 TO BUILD THE PROVER:
03100 THE PROVER CAN BE CREATED IN 37K.USING 2000 FULL WORDS AND 36000 BPS.
03200 THIS IS AN EXTRA LARGE PORTION OF BPS BUT IS USEFUL FOR PATCHING WITHOUT
03300 RECOMPILING THE WHOLE SYSTEM.
03400 THE ORDER OF LOADING SHOULD BE:
03500 PROVE1.LAP,MATCHER.LAP,SDIO.LAP,SCAN.REL,PRIM.REL,UNIF.REL,STATEV.NEW,PROVER.PRM
03550 NOTE: THE REL FILES SHOULD BE ENTERED VIA "(LOAD T)".
03600 AT THIS POINT (PRINIT)MAY BE EXECUTED.
03700 NOW THE SDIO: COMMAND.LAP,EDIT.LAP,MATCH.LAP,INFIX.LAP,FIX.LAP
03800 (FIX.LAP SHOUL COME LAST).